Nuprl Lemma : fshift_increasing
4,23
postcript
pdf
n
:
,
x
:
,
f
:(
n
). increasing(
f
;
n
)
0<
n
x
<
f
(0)
increasing(fshift(
f
;
x
);
n
+1)
latex
Definitions
fshift(
f
;
x
)
,
increasing(
f
;
k
)
,
if
b
t
else
f
fi
,
Unit
,
P
Q
,
i
=
j
,
False
,
P
Q
,
i
j
<
k
,
P
&
Q
,
A
B
,
,
b
,
Prop
,
A
,
t
T
,
b
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
,
SQType(
T
)
,
{
T
}
Lemmas
assert
wf
,
not
wf
,
bnot
wf
,
le
wf
,
eq
int
wf
,
assert
of
eq
int
,
not
functionality
wrt
iff
,
assert
of
bnot
,
iff
transitivity
,
eqff
to
assert
,
eqtt
to
assert
,
bool
wf
,
nat
wf
,
int
seg
wf
origin
n:
, x:
, f:(n
). increasing(f;n) 
0<n x<f(0) increasing(fshift(f;x);n+1) n:, x:, f:(n). increasing(f;n) 0<n x<f(0) increasing(fshift(f;x);n+1) 
t else f fi
Q
j Q
j < kB
bA
T
bx:A. B(x)
}